H-Termination proof of /home/matraf/haskell/eval_FullyBlown

YES 0.685 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/FiniteMap.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:

↳ HASKELL

  ↳ LR

mainModule FiniteMap

((eltsFM :: FiniteMap b a -> [a]) :: FiniteMap b a -> [a])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

eltsFM :: FiniteMap b a -> [a]

eltsFM

foldFM (\key elt rest ->elt : rest) [] fm

foldFM :: (b -> c -> a -> a) -> a -> FiniteMap b c -> a

foldFM	k z EmptyFM	=	z
foldFM	k z (Branch key elt _ fm_l fm_r)	=	foldFM k (k key elt (foldFM k z fm_r)) fm_l

module Maybe where

import qualified FiniteMap
import qualified Prelude

Lambda Reductions:
The following Lambda expression

\keyeltrest→elt : rest

is transformed to

eltsFM0 key elt rest = elt : rest

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

mainModule FiniteMap

((eltsFM :: FiniteMap a b -> [b]) :: FiniteMap a b -> [b])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap a b = EmptyFM | Branch a b Int (FiniteMap a b) (FiniteMap a b)

eltsFM :: FiniteMap b a -> [a]

eltsFM

foldFM eltsFM0 [] fm

eltsFM0

key elt rest

elt : rest

foldFM :: (c -> a -> b -> b) -> b -> FiniteMap c a -> b

foldFM	k z EmptyFM	=	z
foldFM	k z (Branch key elt _ fm_l fm_r)	=	foldFM k (k key elt (foldFM k z fm_r)) fm_l

module Maybe where

import qualified FiniteMap
import qualified Prelude

Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

mainModule FiniteMap

((eltsFM :: FiniteMap a b -> [b]) :: FiniteMap a b -> [b])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

eltsFM :: FiniteMap a b -> [b]

eltsFM

foldFM eltsFM0 [] fm

eltsFM0

key elt rest

elt : rest

foldFM :: (c -> b -> a -> a) -> a -> FiniteMap c b -> a

foldFM	k z EmptyFM	=	z
foldFM	k z (Branch key elt vw fm_l fm_r)	=	foldFM k (k key elt (foldFM k z fm_r)) fm_l

module Maybe where

import qualified FiniteMap
import qualified Prelude

Cond Reductions:
The following Function with conditions

undefined

| False

= undefined

is transformed to

undefined = undefined1

undefined0 True = undefined

undefined1 = undefined0 False

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

mainModule FiniteMap

(eltsFM :: FiniteMap b a -> [a])

module FiniteMap where

import qualified Maybe
import qualified Prelude

data FiniteMap b a = EmptyFM | Branch b a Int (FiniteMap b a) (FiniteMap b a)

eltsFM :: FiniteMap a b -> [b]

eltsFM

foldFM eltsFM0 [] fm

eltsFM0

key elt rest

elt : rest

foldFM :: (b -> c -> a -> a) -> a -> FiniteMap b c -> a

foldFM	k z EmptyFM	=	z
foldFM	k z (Branch key elt vw fm_l fm_r)	=	foldFM k (k key elt (foldFM k z fm_r)) fm_l

module Maybe where

import qualified FiniteMap
import qualified Prelude

Haskell To QDPs

digraph dp_graph {
node [outthreshold=100, inthreshold=100];1[label="eltsFM",fontsize=16,color="grey",shape="box"];1 -> 3[label="",style="dashed", color="grey", weight=3];
3[label="eltsFM vz3",fontsize=16,color="black",shape="triangle"];3 -> 4[label="",style="solid", color="black", weight=3];
4[label="foldFM eltsFM0 [] vz3",fontsize=16,color="burlywood",shape="triangle"];22[label="vz3/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];4 -> 22[label="",style="solid", color="burlywood", weight=9];
22 -> 5[label="",style="solid", color="burlywood", weight=3];
23[label="vz3/Branch vz30 vz31 vz32 vz33 vz34",fontsize=10,color="white",style="solid",shape="box"];4 -> 23[label="",style="solid", color="burlywood", weight=9];
23 -> 6[label="",style="solid", color="burlywood", weight=3];
5[label="foldFM eltsFM0 [] EmptyFM",fontsize=16,color="black",shape="box"];5 -> 7[label="",style="solid", color="black", weight=3];
6[label="foldFM eltsFM0 [] (Branch vz30 vz31 vz32 vz33 vz34)",fontsize=16,color="black",shape="box"];6 -> 8[label="",style="solid", color="black", weight=3];
7[label="[]",fontsize=16,color="green",shape="box"];8 -> 9[label="",style="dashed", color="red", weight=0];
8[label="foldFM eltsFM0 (eltsFM0 vz30 vz31 (foldFM eltsFM0 [] vz34)) vz33",fontsize=16,color="magenta"];8 -> 10[label="",style="dashed", color="magenta", weight=3];
10 -> 4[label="",style="dashed", color="red", weight=0];
10[label="foldFM eltsFM0 [] vz34",fontsize=16,color="magenta"];10 -> 11[label="",style="dashed", color="magenta", weight=3];
9[label="foldFM eltsFM0 (eltsFM0 vz30 vz31 vz4) vz33",fontsize=16,color="burlywood",shape="triangle"];26[label="vz33/EmptyFM",fontsize=10,color="white",style="solid",shape="box"];9 -> 26[label="",style="solid", color="burlywood", weight=9];
26 -> 12[label="",style="solid", color="burlywood", weight=3];
27[label="vz33/Branch vz330 vz331 vz332 vz333 vz334",fontsize=10,color="white",style="solid",shape="box"];9 -> 27[label="",style="solid", color="burlywood", weight=9];
27 -> 13[label="",style="solid", color="burlywood", weight=3];
11[label="vz34",fontsize=16,color="green",shape="box"];12[label="foldFM eltsFM0 (eltsFM0 vz30 vz31 vz4) EmptyFM",fontsize=16,color="black",shape="box"];12 -> 14[label="",style="solid", color="black", weight=3];
13[label="foldFM eltsFM0 (eltsFM0 vz30 vz31 vz4) (Branch vz330 vz331 vz332 vz333 vz334)",fontsize=16,color="black",shape="box"];13 -> 15[label="",style="solid", color="black", weight=3];
14[label="eltsFM0 vz30 vz31 vz4",fontsize=16,color="black",shape="box"];14 -> 16[label="",style="solid", color="black", weight=3];
15 -> 9[label="",style="dashed", color="red", weight=0];
15[label="foldFM eltsFM0 (eltsFM0 vz330 vz331 (foldFM eltsFM0 (eltsFM0 vz30 vz31 vz4) vz334)) vz333",fontsize=16,color="magenta"];15 -> 17[label="",style="dashed", color="magenta", weight=3];
15 -> 18[label="",style="dashed", color="magenta", weight=3];
15 -> 19[label="",style="dashed", color="magenta", weight=3];
15 -> 20[label="",style="dashed", color="magenta", weight=3];
16[label="vz31 : vz4",fontsize=16,color="green",shape="box"];17 -> 9[label="",style="dashed", color="red", weight=0];
17[label="foldFM eltsFM0 (eltsFM0 vz30 vz31 vz4) vz334",fontsize=16,color="magenta"];17 -> 21[label="",style="dashed", color="magenta", weight=3];
18[label="vz333",fontsize=16,color="green",shape="box"];19[label="vz330",fontsize=16,color="green",shape="box"];20[label="vz331",fontsize=16,color="green",shape="box"];21[label="vz334",fontsize=16,color="green",shape="box"];}

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                    ↳ QDPSizeChangeProof

                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_foldFM(vz30, vz31, vz4, Branch(vz330, vz331, vz332, vz333, vz334), h, ba) → new_foldFM(vz330, vz331, new_foldFM0(vz30, vz31, vz4, vz334, h, ba), vz333, h, ba)
new_foldFM(vz30, vz31, vz4, Branch(vz330, vz331, vz332, vz333, vz334), h, ba) → new_foldFM(vz30, vz31, vz4, vz334, h, ba)

The TRS R consists of the following rules:

new_foldFM0(vz30, vz31, vz4, Branch(vz330, vz331, vz332, vz333, vz334), h, ba) → new_foldFM0(vz330, vz331, new_foldFM0(vz30, vz31, vz4, vz334, h, ba), vz333, h, ba)
new_foldFM0(vz30, vz31, vz4, EmptyFM, h, ba) → :(vz31, vz4)

The set Q consists of the following terms:

new_foldFM0(x0, x1, x2, EmptyFM, x3, x4)
new_foldFM0(x0, x1, x2, Branch(x3, x4, x5, x6, x7), x8, x9)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM(vz30, vz31, vz4, Branch(vz330, vz331, vz332, vz333, vz334), h, ba) → new_foldFM(vz330, vz331, new_foldFM0(vz30, vz31, vz4, vz334, h, ba), vz333, h, ba)
The graph contains the following edges 4 > 1, 4 > 2, 4 > 4, 5 >= 5, 6 >= 6
new_foldFM(vz30, vz31, vz4, Branch(vz330, vz331, vz332, vz333, vz334), h, ba) → new_foldFM(vz30, vz31, vz4, vz334, h, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 > 4, 5 >= 5, 6 >= 6

↳ HASKELL

  ↳ LR

    ↳ HASKELL

      ↳ BR

        ↳ HASKELL

          ↳ COR

            ↳ HASKELL

              ↳ Narrow

                ↳ AND

                  ↳ QDP

                  ↳ QDP

                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_foldFM1(Branch(vz30, vz31, vz32, vz33, vz34), h, ba) → new_foldFM1(vz34, h, ba)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

new_foldFM1(Branch(vz30, vz31, vz32, vz33, vz34), h, ba) → new_foldFM1(vz34, h, ba)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3